Nuprl Definition : l_all
11,40
postcript
pdf
l_all(
L
;
T
;
x
.
P
(
x
)) ==
x
:
T
. (
x
L
)
P
(
x
)
latex
clarification:
l_all(
L
;
T
;
x
.
P
(
x
)) ==
x
:
T
. (
x
L
T
)
P
(
x
)
latex
Definitions
x
:
A
.
B
(
x
)
,
P
Q
,
(
x
l
)
FDL editor aliases
l_all
origin
x:T. (x 
L) 
P(x)
x:T. (x L T) P(x) x:T. (x L) P(x)
x:T. (x L T) P(x) x:A. B(x) Q l)